package kodkod.analysis.ordering;

import java.text.DecimalFormat;
import java.text.DecimalFormatSymbols;
import java.text.NumberFormat;
import java.util.ArrayList;

import kodkod.analysis.Analyzer;
import kodkod.analysis.OrderableSolver;
import kodkod.ast.Relation;
import kodkod.engine.fol2sat.Translation;

public class SteplikePromotion extends AbstractOrdering {
	
	Analyzer analyzer = null;
	double baseline = 0.0;
	double factor = 1.0;

	public SteplikePromotion() {
		this(null);
	}
	
	public SteplikePromotion(Analyzer analyzer) {
		super();
		this.analyzer = analyzer;
	}
	
	public SteplikePromotion(Analyzer analyzer, double baseline, double factor) {
		super();
		this.analyzer = analyzer;
		this.baseline = baseline;
		this.factor = factor;
	}
	
	public void apply(Translation translation) {
		if (analyzer == null) {
			analyzer = new Analyzer(translation);
		}
		
		ArrayList<Integer> indices = analyzer.getRelationIdsOrdered();
		ArrayList<Double> weights = analyzer.getRelationWeightsOrdered();
		double weight0 = weights.get(0);
		
		for (int pos = 0; pos < indices.size(); pos++) {
			Relation rel = translation.primaryRelations.get(indices.get(pos));
			int[] vars = translation.primaryVariables(rel).toArray();
			double weight = baseline + factor * weights.get(pos) / weight0;
			
			for (int var : vars) {
				weightVariable((OrderableSolver)translation.cnf(), var, weight);
			}
		}
	}
	
	public String toString() {
		if (softOrder) {
			StringBuffer buf = new StringBuffer();
			buf.append("SteplikeInitialize");
			DecimalFormatSymbols symbols = new DecimalFormatSymbols();
			symbols.setDecimalSeparator('.');
			NumberFormat format = new DecimalFormat("#0.00", symbols);
			buf.append("-");
			buf.append(format.format(baseline));
			buf.append("-");
			buf.append(format.format(factor));
			return buf.toString();
		} else {
			return "UniformOverride";
		}
	}
}
